import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes

IntArray = symtypes.tdict(simsym.SInt, ptypes.APREF)

class ProcessQueue(simsym.tstruct(
		elts = IntArray,
		head = simsym.SInt,
		tail = simsym.SInt,
		tmp = simsym.SInt
		)):
	def _declare_assumptions(self, assume):
		super(ProcessQueue, self)._declare_assumptions(assume)
		assume(self.head <= self.tail)
	
	@model.methodwrap()
	def INIT(self):
		self.head = 1
		self.tail = 1
	
	@model.methodwrap()
	def isEmpty(self):
		if self.head < self.tail:
			return True
		return False
	
	@model.methodwrap(x = ptypes.APREF)
	def Enqueue(self, x):
		self.elts._map[self.tail] = x
		self.tail = self.tail + 1
	
	@model.methodwrap()
	def RemoveFirst(self):
		self.head = self.head + 1
		return self.elts._map[self.head - 1]
	
	@model.methodwrap()
	def QueueFront(self):
		return self.elts._map[self.head]

	@model.methodwrap(x = ptypes.APREF)
	def RemoveElement(self, x):
		# XXX UA run too slow on this function
		return
		i = self.head
		while (i < self.tail):
			if (self.elts._map[i] == x):
				j = i;
				while (j < self.tail - 1):
					self.elts._map[j] = self.elts._map[j + 1]
					j = j + 1
				self.tail = self.tail - 1
				return True
			i = i + 1
		return False
model_class = ProcessQueue
